The closed unit ball of the double dual of a Banach space is weak* compact. This theorem is equivalent to the Tychonoff theorem for compact Hausdorff spaces (eg Rossi 2009), and as such is not constructive in general. However, the restriction of the statement to separable Banach spaces is constructive, and is used in PDE theory to find solutions. A constructive proof can be found e.g. in BridgesVita.
As usual, when formulating the theorem using locales instead of topological spaces the theorem holds constructively; see Pelletier and Henry.
The following is a generalisation to locally convex spaces:
Wikipedia, Banach–Alaoglu theorem
Stefano Rossi, The Banach-Alaoglu theorem is equivalent to the Tychonoff theorem for compact Hausdorff spaces, arXiv:0911.0332
Joan Wick Pelletier, Locales in functional analysis DOI
Simon Henry, Localic Metric spaces and the localic Gelfand duality arxiv
Bridges and Vita, Techniques of Constructive Analysis link
Last revised on June 7, 2017 at 03:40:04. See the history of this page for a list of all contributions to it.